Nuprl Lemma : rcv-from-on_wf 0,22
E, X1, X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), info:(E(IdX1+(IdLnkE)X2)), e, r:E,
l:IdLnk.
rcv-from-on(dE;dL;info;e;l;r)   
latex

Definitionsrcv?(e), Id, EqDecider(T), rcv-from-on(dE;dL;info;e;l;r), Unit, P  Q, P & Q, b, , p  q, sender(e), eqof(d), IdLnk, link(e), x:A. B(x), P  Q, t  T
Lemmaslink wf, eqof wf, sender wf, band wf, bool wf, rcv? wf, eqtt to assert, deq wf, IdLnk wf, Id wf

origin